k:Knd, T,B:Type, l:IdLnk, ds:fpf(Id; x.Type), tg:Id, f:(decl-state(ds)TB).
((isrcv(k))
 ((destination(lnk(k)) = source(l)  Id)  ((lnk(k) = l)  ((T = B)  (tag(k) = tg)))))
 normal-ds{i:l}
 normal-ds(ds)
 normal-type{i:l}
 normal-type(T)
 normal-type{i:l}
 normal-type(B)
 es-real{i:l}
 es-real(es.usends1-p(es;ds;k;T;l;tg;B;f)) 

latex

Definitions	x. t(x), prop{i:l}, top, decl-type{i:l}(ds; x), t  T, x:A. B(x), es-real{i:l}(es.P(es)), P  Q, P  Q, x:A. B(x), x(s)
Lemmas	Knd wf, fpf wf, decl-state wf, tagof wf, IdLnk wf, lsrc wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, normal-ds wf, normal-type wf, event system wf, usends1-p wf, R-realizes wf, R-usends1-rule, decl-type wf, id-deq wf, fpf-cap-single1, Rsends wf, fpf-single wf3